A, C, B:Type, eqa:EqDecider(A), eqc, eqc':EqDecider(C), r:(AC), f:a:A fp B, a:A, z:B, c:C.
Inj(A;C;r)  (c = r(a))  (rename(r;f)(c)?z = f(a)?z  B) 

latex

Definitions	x:A. B(x), P  Q, t  T, , x. t(x), x(s)
Lemmas	fpf-cap wf, inject wf, fpf wf, deq wf, fpf-rename-cap2, fpf-rename wf